M1, M2:MsgA, l:IdLnk. M1  M2 sends on link l  M1 sends on link l  M2 sends on link l 

latex

Definitions	M sends on link l, M1  M2, mk-ma, x:A. B(x), P  Q, P  Q, left+right, IdLnk, x:AB(x), t  T, MsgA, Valtype(da;k), f  g, x  dom(f), a:A fp B(a), x:AB(x), b, deq-member(eq;x;L), IdLnkDeq, map(f;as), x.A(x), 2of(t), Dec(P), type List, T, True, as @ bs, A, False, {T}, x:A. B(x), Prop, filter(P;l), A & B, Type, s = t, f(a), (x  l), x. t(x), P  Q, P  Q, b, product-deq(A;B;a;b), KindDeq, Knd, P & Q, Void
Lemmas	not wf, assert of bnot, iff transitivity, IdLnk wf, Knd wf, idlnk-deq wf, Kind-deq wf, product-deq wf, deq-member wf, bnot wf, member filter, pi2 wf, filter wf, l member wf, member map, map wf, append wf, member append, iff functionality wrt iff, map append, true wf, squash wf, iff wf, assert wf, assert-deq-member, or functionality wrt iff, not functionality wrt iff, decidable assert, msga wf